i, x:Id, k:Knd, ds:x:Id fp Type, T:Type, f:(State(ds)Tds(x)?Void).
(isrcv(k)  i = destination(lnk(k)))
 @i: with declarations 
 ds:ds
 da:k : T

 effect of k(v) is x := f s v 
 realizes es.
 @i events of kind k change x to f State(ds) (val:T) 

latex

Definitions

Void, t  T, x:A. B(x), Top, KindDeq, P  Q, x:A. B(x), Knd, Valtype(da;k), {T}, SQType(T), s = t, Prop, s ~ t, left+right, x:AB(x), Id, Type, f(x)?z, ES(the_w), E, P  Q, x:AB(x), P & Q, P  Q, valtype(e), kindtype(i;k), loc(e), kind(e), f(a), (x after e), <a,b>, A & B, vartype(i;x), e@i. P(e), @i events of kind k change x to f State(ds) (val:T), PossibleWorld(D;w), FairFifo, World, S  T, IdDeq, x.A(x), x. t(x), State(ds), S  T, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, D1  D2, Dsys, D realizes es. P(es), lnk(k), destination(l), isrcv(k), b, a:A fp B(a), x : v

Lemmas

effect-rule, fpf wf, assert wf, isrcv wf, ldst wf, lnk wf, dsys wf, d-sub wf, d-single-effect wf, ma-valtype wf, fpf-single wf, ma-state wf, fpf-cap wf, id-deq wf, world wf, fair-fifo wf, possible-world wf, es-kind wf, Id wf, es-loc wf, es-E wf, w-es wf, Knd sq, fpf-cap-single1, Knd wf, Kind-deq wf